Termination w.r.t. Q of the following Term Rewriting System could be disproven:

Q restricted rewrite system:
The TRS R consists of the following rules:

h(X) → g(X, X)
g(a, X) → f(b, activate(X))
f(X, X) → h(a)
a → b
activate(X) → X

Q is empty.


↳ QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

h(X) → g(X, X)
g(a, X) → f(b, activate(X))
f(X, X) → h(a)
a → b
activate(X) → X

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

G(a, X) → F(b, activate(X))
F(X, X) → H(a)
F(X, X) → A
G(a, X) → ACTIVATE(X)
H(X) → G(X, X)

The TRS R consists of the following rules:

h(X) → g(X, X)
g(a, X) → f(b, activate(X))
f(X, X) → h(a)
a → b
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

G(a, X) → F(b, activate(X))
F(X, X) → H(a)
F(X, X) → A
G(a, X) → ACTIVATE(X)
H(X) → G(X, X)

The TRS R consists of the following rules:

h(X) → g(X, X)
g(a, X) → f(b, activate(X))
f(X, X) → h(a)
a → b
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesReductionPairsProof

Q DP problem:
The TRS P consists of the following rules:

G(a, X) → F(b, activate(X))
F(X, X) → H(a)
H(X) → G(X, X)

The TRS R consists of the following rules:

h(X) → g(X, X)
g(a, X) → f(b, activate(X))
f(X, X) → h(a)
a → b
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(F(x1, x2)) = x1 + x2   
POL(G(x1, x2)) = x1 + x2   
POL(H(x1)) = 2·x1   
POL(a) = 0   
POL(activate(x1)) = x1   
POL(b) = 0   



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesReductionPairsProof
            ↳ QDP
              ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

G(a, X) → F(b, activate(X))
F(X, X) → H(a)
H(X) → G(X, X)

The TRS R consists of the following rules:

a → b
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule G(a, X) → F(b, activate(X)) at position [] we obtained the following new rules:

G(a, x0) → F(b, x0)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesReductionPairsProof
            ↳ QDP
              ↳ Narrowing
                ↳ QDP
                  ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

F(X, X) → H(a)
G(a, x0) → F(b, x0)
H(X) → G(X, X)

The TRS R consists of the following rules:

a → b
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule F(X, X) → H(a) we obtained the following new rules:

F(b, b) → H(a)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesReductionPairsProof
            ↳ QDP
              ↳ Narrowing
                ↳ QDP
                  ↳ Instantiation
                    ↳ QDP
                      ↳ UsableRulesReductionPairsProof

Q DP problem:
The TRS P consists of the following rules:

F(b, b) → H(a)
G(a, x0) → F(b, x0)
H(X) → G(X, X)

The TRS R consists of the following rules:

a → b
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(F(x1, x2)) = x1 + x2   
POL(G(x1, x2)) = x1 + x2   
POL(H(x1)) = 2·x1   
POL(a) = 0   
POL(b) = 0   



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesReductionPairsProof
            ↳ QDP
              ↳ Narrowing
                ↳ QDP
                  ↳ Instantiation
                    ↳ QDP
                      ↳ UsableRulesReductionPairsProof
                        ↳ QDP
                          ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

F(b, b) → H(a)
G(a, x0) → F(b, x0)
H(X) → G(X, X)

The TRS R consists of the following rules:

a → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule H(X) → G(X, X) we obtained the following new rules:

H(a) → G(a, a)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesReductionPairsProof
            ↳ QDP
              ↳ Narrowing
                ↳ QDP
                  ↳ Instantiation
                    ↳ QDP
                      ↳ UsableRulesReductionPairsProof
                        ↳ QDP
                          ↳ ForwardInstantiation
                            ↳ QDP
                              ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

F(b, b) → H(a)
H(a) → G(a, a)
G(a, x0) → F(b, x0)

The TRS R consists of the following rules:

a → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

F(b, b) → H(a)
H(a) → G(a, a)
G(a, x0) → F(b, x0)

The TRS R consists of the following rules:

a → b


s = H(a) evaluates to t =H(a)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

H(a) → G(a, a)
with rule H(a) → G(a, a) at position [] and matcher [ ]

G(a, a) → G(a, b)
with rule a → b at position [1] and matcher [ ]

G(a, b) → F(b, b)
with rule G(a, x0) → F(b, x0) at position [] and matcher [x0 / b]

F(b, b) → H(a)
with rule F(b, b) → H(a)

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.